﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;

namespace Logic
{
	class MinesAgent
	{
		MinesHost host;
		CNFSentence kb;
		Random rand;
		bool isDead, isSolved, isAlreadyCheated;
        //TODO: make a struct {x,y}
		List<Tuple<int, int>> openedCells = new List<Tuple<int, int>>();
        List<Tuple<int, int>> cellsToRandomChoose = new List<Tuple<int, int>>();

		public bool IsDead { get { return isDead; } }
        public bool IsSolved { get { return isSolved; } }

		public MinesAgent(MinesHost host)
		{			
			this.host = host;
			List<string> v = new List<string>();

			//It's cumbersome to create logical expressions about mines, when we're near the border,
			//so here's a nice workaround - we append propositional symbols about mines, that lie 1 cell outside,
			//and then tell the knowledge base, that they're always false
			for (int y = -1; y < host.SizeY+1; y++)				
				for(int x = -1; x < host.SizeX+1; x++)				
					v.Add("M" + x + "," + y);

            for (int y = 0; y < host.SizeY; y++)
                for (int x = 0; x < host.SizeX; x++)
                    cellsToRandomChoose.Add(new Tuple<int, int>(x, y));


			kb = new CNFSentence(new LogicalSystem(v));
            
			for (int y = -1; y < host.SizeY + 1; y++)
			{
				kb.AppendClause(new List<int>() { ~GetMineVariable(-1, y) });
				kb.AppendClause(new List<int>() { ~GetMineVariable(host.SizeX, y) });
			}

			for (int x = 0; x < host.SizeX; x++)
			{
				kb.AppendClause(new List<int>() { ~GetMineVariable(x, -1) });
				kb.AppendClause(new List<int>() { ~GetMineVariable(x, host.SizeY) });
			}



            rand = new Random(); //4);
			isDead = false;
		}	
		
		public void Act()
		{			
			if (isDead) return;

			

			List<int[]> safeCells = new List<int[]>();

			int totalOpenedNodes = 0;           
            Stopwatch sw = new Stopwatch();
            sw.Start();
			//For every non-opened cell in the map...
            int[] cachedSolution = null;
			for (int tx = 0; tx < host.SizeX; tx++)
			{         
				for (int ty = 0; ty < host.SizeY; ty++)
				{                    
					if (openedCells.Any(x => x.Item1 == tx && x.Item2 == ty)) continue;
                    Console.CursorLeft = Console.CursorTop = 0;    
                    Console.WriteLine("Thinking... checking " + tx + "," + ty + "               ");
					SATSolver solver = new SATSolver();
					CNFSentence tryContr = (CNFSentence)kb.Clone();
					tryContr.AppendClause(new List<int>() { GetMineVariable(tx, ty) });					

					//...try to prove, that ~Mx,y by checking that KB & Mx,y is unsatisfiable.
					int[] solution = solver.Solve(tryContr, cachedSolution);
                    if (solution == null)
                        safeCells.Add(new[] { tx, ty });
                    else
                        cachedSolution = solution;
                    totalOpenedNodes += solver.NodesExpanded;
				}				
			}
            sw.Stop();

			Console.CursorLeft = Console.CursorTop = 0;
			Console.WriteLine("Done... total opened nodes: " + totalOpenedNodes + "                   ");
            Console.WriteLine("Think time: " + sw.ElapsedMilliseconds + " ms                      ");
            Console.WriteLine("Knowledge base size: " + kb.Formula.Count + " clauses (" 
                + kb.Formula.Count(x => x.Count > 1) + " non-unit), " + kb.VariableIndex.Count + " variables             ");
			Console.WriteLine("Found " + safeCells.Count + " safe cells                              ");

			if (safeCells.Count == 0) //TODO: maybe try to prove mines?
			{
                if (!isAlreadyCheated)
                {
                    safeCells.Add(host.CheatPleaseGiveMeZero());
                    isAlreadyCheated = true;
                }
                else
                {
                    if (cellsToRandomChoose.Count == 0) { isSolved = true; return; }
                    var rnd = cellsToRandomChoose[rand.Next(cellsToRandomChoose.Count)];
                    safeCells.Add(new[] { rnd.Item1, rnd.Item2 });
                }
			}
			

			foreach (int[] oc in safeCells)
			{
				int tx = oc[0];
				int ty = oc[1];
				int c = host.Open(tx, ty);
				openedCells.Add(new Tuple<int, int>(tx, ty));
                cellsToRandomChoose.Remove(new Tuple<int, int>(tx, ty));
				if (c == -1) 
                { 
                    isDead = true; return; 
                }
				kb.AppendClause(new List<int>() { ~GetMineVariable(tx, ty) });

				LogicalSystem ls = new LogicalSystem(Enumerable.Range(0, 8).Select(_ => _.ToString()));
				CNFSentence minesAround = CNFSentence.FromTruthTable(ls, GetMinesFunction(c), 8);

				List<Tuple<int, int>> convert = new List<Tuple<int, int>>();
				for (int i = 0; i < 8; i++)
				{
					int ax = tx + host.Directions[i, 0];
					int ay = ty + host.Directions[i, 1];
					int var = GetMineVariable(ax, ay);
					convert.Add(new Tuple<int, int>(i, var));
				}
				minesAround.ChangeVariableSet(kb.LogicalSystem, convert);
				kb.Append(minesAround);				
			}

			kb.Compact();
			kb.BuildIndex();

            //Remove confirmed mines
            foreach (var cl in kb.Formula.Where(x => x.Count == 1 && x[0] > 0))
            {                
                int[] c = GetCoordsFromVariable(cl[0]);               
                cellsToRandomChoose.Remove(new Tuple<int, int>(c[0]-1, c[1]-1));                
            }
		}

		public void DrawFacts()
		{
			int[,] facts = new int[host.SizeX+2, host.SizeY+2];
			foreach(var cl in kb.Formula.Where(x => x.Count == 1))
			{
				int v = cl[0];
				bool neg = false;
				if(v < 0)
				{
					v = ~v;
					neg  = true;
				}
				
				int[] c = GetCoordsFromVariable(v);

				facts[c[0],c[1]] = neg ? -1 : 1;
			}
			for(int y = 1; y < host.SizeY+1; y++)
			{
				for(int x = 1; x < host.SizeX+1; x++)
				{
					if(facts[x,y] == -1)
						Console.ForegroundColor = ConsoleColor.Blue;
					else if(facts[x,y] == 1)
						Console.ForegroundColor = ConsoleColor.Red;
					Console.Write("0 ");
					Console.ForegroundColor = ConsoleColor.Gray;
				}
				Console.WriteLine();
			}

			Console.WriteLine();

			//foreach (var cl in kb.Formula.Where(x => x.Count > 1))
			//{
			//    foreach (int v in cl)
			//    {
			//        int vv = v;
			//        if (vv < 0)
			//        {
			//            Console.Write("~");
			//            vv = ~vv;
			//        }
			//        Console.Write(kb.LogicalSystem.Symbols[vv] + " ");
			//    }
			//    Console.WriteLine();
			//}
		}

		int GetMineVariable(int x, int y)
		{
			return (y + 1) * (host.SizeX + 2) + (x + 1);
		}

		int[] GetCoordsFromVariable(int v)
		{
			int[] c = new int[2];
			c[0] = v % (host.SizeX + 2);
			c[1] = v / (host.SizeX + 2);
			return c;
		}

		Func<int[], bool> GetMinesFunction(int count)
		{
			return x =>
			    {
			        int c = 0;
			        for (int i = 0; i < 8; i++)
			            if (x[i] == 1) c++;
			        return c == count;
			    };
		}
	}
}
